The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

revconsapp(C(x1, x2), r) → revconsapp(x2, C(x1, r))
deeprevapp(C(x1, x2), rest) → deeprevapp(x2, C(x1, rest))
deeprevapp(V(n), rest) → revconsapp(rest, V(n))
deeprevapp(N, rest) → rest
revconsapp(V(n), r) → r
revconsapp(N, r) → r
deeprev(C(x1, x2)) → deeprevapp(C(x1, x2), N)
deeprev(V(n)) → V(n)
deeprev(N) → N
second(V(n)) → N
second(C(x1, x2)) → x2
isVal(C(x1, x2)) → False
isVal(V(n)) → True
isVal(N) → False
isNotEmptyT(C(x1, x2)) → True
isNotEmptyT(V(n)) → False
isNotEmptyT(N) → False
isEmptyT(C(x1, x2)) → False
isEmptyT(V(n)) → False
isEmptyT(N) → True
first(V(n)) → N
first(C(x1, x2)) → x1
goal(x) → deeprev(x)

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^1).


The TRS R consists of the following rules:

revconsapp(C(x1, x2), r) → revconsapp(x2, C(x1, r)) [1]
deeprevapp(C(x1, x2), rest) → deeprevapp(x2, C(x1, rest)) [1]
deeprevapp(V(n), rest) → revconsapp(rest, V(n)) [1]
deeprevapp(N, rest) → rest [1]
revconsapp(V(n), r) → r [1]
revconsapp(N, r) → r [1]
deeprev(C(x1, x2)) → deeprevapp(C(x1, x2), N) [1]
deeprev(V(n)) → V(n) [1]
deeprev(N) → N [1]
second(V(n)) → N [1]
second(C(x1, x2)) → x2 [1]
isVal(C(x1, x2)) → False [1]
isVal(V(n)) → True [1]
isVal(N) → False [1]
isNotEmptyT(C(x1, x2)) → True [1]
isNotEmptyT(V(n)) → False [1]
isNotEmptyT(N) → False [1]
isEmptyT(C(x1, x2)) → False [1]
isEmptyT(V(n)) → False [1]
isEmptyT(N) → True [1]
first(V(n)) → N [1]
first(C(x1, x2)) → x1 [1]
goal(x) → deeprev(x) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

revconsapp(C(x1, x2), r) → revconsapp(x2, C(x1, r)) [1]
deeprevapp(C(x1, x2), rest) → deeprevapp(x2, C(x1, rest)) [1]
deeprevapp(V(n), rest) → revconsapp(rest, V(n)) [1]
deeprevapp(N, rest) → rest [1]
revconsapp(V(n), r) → r [1]
revconsapp(N, r) → r [1]
deeprev(C(x1, x2)) → deeprevapp(C(x1, x2), N) [1]
deeprev(V(n)) → V(n) [1]
deeprev(N) → N [1]
second(V(n)) → N [1]
second(C(x1, x2)) → x2 [1]
isVal(C(x1, x2)) → False [1]
isVal(V(n)) → True [1]
isVal(N) → False [1]
isNotEmptyT(C(x1, x2)) → True [1]
isNotEmptyT(V(n)) → False [1]
isNotEmptyT(N) → False [1]
isEmptyT(C(x1, x2)) → False [1]
isEmptyT(V(n)) → False [1]
isEmptyT(N) → True [1]
first(V(n)) → N [1]
first(C(x1, x2)) → x1 [1]
goal(x) → deeprev(x) [1]

The TRS has the following type information:

revconsapp :: C:V:N → C:V:N → C:V:N C :: C:V:N → C:V:N → C:V:N deeprevapp :: C:V:N → C:V:N → C:V:N V :: a → C:V:N N :: C:V:N deeprev :: C:V:N → C:V:N second :: C:V:N → C:V:N isVal :: C:V:N → False:True False :: False:True True :: False:True isNotEmptyT :: C:V:N → False:True isEmptyT :: C:V:N → False:True first :: C:V:N → C:V:N goal :: C:V:N → C:V:N

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

revconsapp
deeprevapp
deeprev
second
isVal
isNotEmptyT
isEmptyT
first
goal

(c) The following functions are completely defined:
none

Due to the following rules being added:
none

And the following fresh constants:

const

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: revconsapp(C(x1, x2), r) → revconsapp(x2, C(x1, r)) [1] deeprevapp(C(x1, x2), rest) → deeprevapp(x2, C(x1, rest)) [1] deeprevapp(V(n), rest) → revconsapp(rest, V(n)) [1] deeprevapp(N, rest) → rest [1] revconsapp(V(n), r) → r [1] revconsapp(N, r) → r [1] deeprev(C(x1, x2)) → deeprevapp(C(x1, x2), N) [1] deeprev(V(n)) → V(n) [1] deeprev(N) → N [1] second(V(n)) → N [1] second(C(x1, x2)) → x2 [1] isVal(C(x1, x2)) → False [1] isVal(V(n)) → True [1] isVal(N) → False [1] isNotEmptyT(C(x1, x2)) → True [1] isNotEmptyT(V(n)) → False [1] isNotEmptyT(N) → False [1] isEmptyT(C(x1, x2)) → False [1] isEmptyT(V(n)) → False [1] isEmptyT(N) → True [1] first(V(n)) → N [1] first(C(x1, x2)) → x1 [1] goal(x) → deeprev(x) [1] The TRS has the following type information: revconsapp :: C:V:N → C:V:N → C:V:N C :: C:V:N → C:V:N → C:V:N deeprevapp :: C:V:N → C:V:N → C:V:N V :: a → C:V:N N :: C:V:N deeprev :: C:V:N → C:V:N second :: C:V:N → C:V:N isVal :: C:V:N → False:True False :: False:True True :: False:True isNotEmptyT :: C:V:N → False:True isEmptyT :: C:V:N → False:True first :: C:V:N → C:V:N goal :: C:V:N → C:V:N const :: a Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: revconsapp(C(x1, x2), r) → revconsapp(x2, C(x1, r)) [1] deeprevapp(C(x1, x2), rest) → deeprevapp(x2, C(x1, rest)) [1] deeprevapp(V(n), rest) → revconsapp(rest, V(n)) [1] deeprevapp(N, rest) → rest [1] revconsapp(V(n), r) → r [1] revconsapp(N, r) → r [1] deeprev(C(x1, x2)) → deeprevapp(C(x1, x2), N) [1] deeprev(V(n)) → V(n) [1] deeprev(N) → N [1] second(V(n)) → N [1] second(C(x1, x2)) → x2 [1] isVal(C(x1, x2)) → False [1] isVal(V(n)) → True [1] isVal(N) → False [1] isNotEmptyT(C(x1, x2)) → True [1] isNotEmptyT(V(n)) → False [1] isNotEmptyT(N) → False [1] isEmptyT(C(x1, x2)) → False [1] isEmptyT(V(n)) → False [1] isEmptyT(N) → True [1] first(V(n)) → N [1] first(C(x1, x2)) → x1 [1] goal(x) → deeprev(x) [1] The TRS has the following type information: revconsapp :: C:V:N → C:V:N → C:V:N C :: C:V:N → C:V:N → C:V:N deeprevapp :: C:V:N → C:V:N → C:V:N V :: a → C:V:N N :: C:V:N deeprev :: C:V:N → C:V:N second :: C:V:N → C:V:N isVal :: C:V:N → False:True False :: False:True True :: False:True isNotEmptyT :: C:V:N → False:True isEmptyT :: C:V:N → False:True first :: C:V:N → C:V:N goal :: C:V:N → C:V:N const :: a Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

N => 0
False => 0
True => 1
const => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + n :|: n >= 0, z = 1 + n
deeprevapp(z, z') -{ 1 }→ rest :|: z' = rest, rest >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(rest, 1 + n) :|: n >= 0, z' = rest, rest >= 0, z = 1 + n
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + rest) :|: x1 >= 0, z' = rest, z = 1 + x1 + x2, rest >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: n >= 0, z = 1 + n
goal(z) -{ 1 }→ deeprev(x) :|: x >= 0, z = x
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: n >= 0, z = 1 + n
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: n >= 0, z = 1 + n
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: n >= 0, z = 1 + n
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ r :|: n >= 0, r >= 0, z = 1 + n, z' = r
revconsapp(z, z') -{ 1 }→ r :|: r >= 0, z = 0, z' = r
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + r) :|: r >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0, z' = r
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: n >= 0, z = 1 + n

(11) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(12) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

(13) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ isNotEmptyT } { isVal } { revconsapp } { isEmptyT } { second } { first } { deeprevapp } { deeprev } { goal }

(14) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {isNotEmptyT}, {isVal}, {revconsapp}, {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}

(15) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: isNotEmptyT
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(16) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {isNotEmptyT}, {isVal}, {revconsapp}, {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: ?, size: O(1) [1]

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: isNotEmptyT
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(18) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {isVal}, {revconsapp}, {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1]

(19) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(20) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {isVal}, {revconsapp}, {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1]

(21) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: isVal
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(22) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {isVal}, {revconsapp}, {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: ?, size: O(1) [1]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: isVal
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(24) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {revconsapp}, {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1]

(25) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(26) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {revconsapp}, {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1]

(27) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: revconsapp
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(28) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {revconsapp}, {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: ?, size: O(n1) [z + z']

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using PUBS for: revconsapp
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + z

(30) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ revconsapp(z', 1 + (z - 1)) :|: z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
revconsapp(z, z') -{ 1 }→ revconsapp(x2, 1 + x1 + z') :|: z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(31) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(32) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z']

(33) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: isEmptyT
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(34) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {isEmptyT}, {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: ?, size: O(1) [1]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: isEmptyT
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(36) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1]

(37) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(38) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1]

(39) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: second
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(40) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {second}, {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: ?, size: O(n1) [z]

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: second
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(42) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z]

(43) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(44) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z]

(45) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using KoAT for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(46) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {first}, {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: ?, size: O(n1) [z]

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: first
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(48) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z]

(49) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(50) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z]

(51) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: deeprevapp
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z + z'

(52) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {deeprevapp}, {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z] deeprevapp: runtime: ?, size: O(n1) [z + z']

(53) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: deeprevapp
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2 + 2·z + z'

(54) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 1 }→ deeprevapp(1 + x1 + x2, 0) :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
deeprevapp(z, z') -{ 1 }→ deeprevapp(x2, 1 + x1 + z') :|: x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z] deeprevapp: runtime: O(n1) [2 + 2·z + z'], size: O(n1) [z + z']

(55) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(56) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 5 + 2·x1 + 2·x2 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + x1 + x2) + 1 * 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 4 + x1 + 2·x2 + z' }→ s'' :|: s'' >= 0, s'' <= 1 * x2 + 1 * (1 + x1 + z'), x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z] deeprevapp: runtime: O(n1) [2 + 2·z + z'], size: O(n1) [z + z']

(57) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: deeprev
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(58) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 5 + 2·x1 + 2·x2 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + x1 + x2) + 1 * 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 4 + x1 + 2·x2 + z' }→ s'' :|: s'' >= 0, s'' <= 1 * x2 + 1 * (1 + x1 + z'), x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {deeprev}, {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z] deeprevapp: runtime: O(n1) [2 + 2·z + z'], size: O(n1) [z + z'] deeprev: runtime: ?, size: O(n1) [z]

(59) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: deeprev
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 3 + 2·z

(60) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 5 + 2·x1 + 2·x2 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + x1 + x2) + 1 * 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 4 + x1 + 2·x2 + z' }→ s'' :|: s'' >= 0, s'' <= 1 * x2 + 1 * (1 + x1 + z'), x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 1 }→ deeprev(z) :|: z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z] deeprevapp: runtime: O(n1) [2 + 2·z + z'], size: O(n1) [z + z'] deeprev: runtime: O(n1) [3 + 2·z], size: O(n1) [z]

(61) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(62) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 5 + 2·x1 + 2·x2 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + x1 + x2) + 1 * 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 4 + x1 + 2·x2 + z' }→ s'' :|: s'' >= 0, s'' <= 1 * x2 + 1 * (1 + x1 + z'), x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 4 + 2·z }→ s2 :|: s2 >= 0, s2 <= 1 * z, z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z] deeprevapp: runtime: O(n1) [2 + 2·z + z'], size: O(n1) [z + z'] deeprev: runtime: O(n1) [3 + 2·z], size: O(n1) [z]

(63) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: goal
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: z

(64) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 5 + 2·x1 + 2·x2 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + x1 + x2) + 1 * 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 4 + x1 + 2·x2 + z' }→ s'' :|: s'' >= 0, s'' <= 1 * x2 + 1 * (1 + x1 + z'), x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 4 + 2·z }→ s2 :|: s2 >= 0, s2 <= 1 * z, z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed: {goal}
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z] deeprevapp: runtime: O(n1) [2 + 2·z + z'], size: O(n1) [z + z'] deeprev: runtime: O(n1) [3 + 2·z], size: O(n1) [z] goal: runtime: ?, size: O(n1) [z]

(65) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: goal
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 4 + 2·z

(66) Obligation:

Complexity RNTS consisting of the following rules:

deeprev(z) -{ 5 + 2·x1 + 2·x2 }→ s1 :|: s1 >= 0, s1 <= 1 * (1 + x1 + x2) + 1 * 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
deeprev(z) -{ 1 }→ 0 :|: z = 0
deeprev(z) -{ 1 }→ 1 + (z - 1) :|: z - 1 >= 0
deeprevapp(z, z') -{ 2 + z' }→ s' :|: s' >= 0, s' <= 1 * z' + 1 * (1 + (z - 1)), z - 1 >= 0, z' >= 0
deeprevapp(z, z') -{ 4 + x1 + 2·x2 + z' }→ s'' :|: s'' >= 0, s'' <= 1 * x2 + 1 * (1 + x1 + z'), x1 >= 0, z = 1 + x1 + x2, z' >= 0, x2 >= 0
deeprevapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
first(z) -{ 1 }→ x1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
first(z) -{ 1 }→ 0 :|: z - 1 >= 0
goal(z) -{ 4 + 2·z }→ s2 :|: s2 >= 0, s2 <= 1 * z, z >= 0
isEmptyT(z) -{ 1 }→ 1 :|: z = 0
isEmptyT(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 1 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z - 1 >= 0
isNotEmptyT(z) -{ 1 }→ 0 :|: z = 0
isVal(z) -{ 1 }→ 1 :|: z - 1 >= 0
isVal(z) -{ 1 }→ 0 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
isVal(z) -{ 1 }→ 0 :|: z = 0
revconsapp(z, z') -{ 2 + x2 }→ s :|: s >= 0, s <= 1 * x2 + 1 * (1 + x1 + z'), z' >= 0, x1 >= 0, z = 1 + x1 + x2, x2 >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z - 1 >= 0, z' >= 0
revconsapp(z, z') -{ 1 }→ z' :|: z' >= 0, z = 0
second(z) -{ 1 }→ x2 :|: x1 >= 0, z = 1 + x1 + x2, x2 >= 0
second(z) -{ 1 }→ 0 :|: z - 1 >= 0

Function symbols to be analyzed:
Previous analysis results are:

isNotEmptyT: runtime: O(1) [1], size: O(1) [1] isVal: runtime: O(1) [1], size: O(1) [1] revconsapp: runtime: O(n1) [1 + z], size: O(n1) [z + z'] isEmptyT: runtime: O(1) [1], size: O(1) [1] second: runtime: O(1) [1], size: O(n1) [z] first: runtime: O(1) [1], size: O(n1) [z] deeprevapp: runtime: O(n1) [2 + 2·z + z'], size: O(n1) [z + z'] deeprev: runtime: O(n1) [3 + 2·z], size: O(n1) [z] goal: runtime: O(n1) [4 + 2·z], size: O(n1) [z]

(67) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(68) BOUNDS(1, n^1)